$\forall$${\it es}$:ES, ${\it Ack}$, ${\it Req}$:(E$\rightarrow\mathbb{P}$), $f$:(\{$e$:E$\mid$ ${\it Ack}$($e$)\} $\rightarrow$\{$e$:E$\mid$ ${\it Req}$($e$)\} ).
\\[0ex]$e$.$f$($e$) is c$<$ preserving on $e$.${\it Ack}$($e$)
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:\{$e$:E$\mid$ ${\it Ack}$($e$)\} . ($\neg$${\it e'}$ c$\leq$ $e$) $\Rightarrow$ ($e$ $<$ ${\it e'}$))
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:\{$e$:E$\mid$ ${\it Req}$($e$)\} . ($\neg$${\it e'}$ c$\leq$ $e$) $\Rightarrow$ ($e$ $<$ ${\it e'}$))
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:\{$e$:E$\mid$ ${\it Req}$($e$)\} . ($e$ $<$ ${\it e'}$) $\Rightarrow$ ($\exists$$a$:\{$e$:E$\mid$ ${\it Ack}$($e$)\} . (($e$ $<$ $a$) \& ($a$ $<$ ${\it e'}$))))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ${\it Req}$($e$) $\Rightarrow$ ($\forall$$a$:E. ${\it Ack}$($a$) $\Rightarrow$ $e$ c$\leq$ $a$ $\Rightarrow$ $e$ c$\leq$ $f$($a$)))